Left Termination of the query pattern ss_in_2(g, a) w.r.t. the given Prolog program could not be shown:



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

Clauses:

ss(Xs, Ys) :- ','(perm(Xs, Ys), ordered(Ys)).
perm([], []).
perm(Xs, .(X, Ys)) :- ','(app(X1s, .(X, X2s), Xs), ','(app(X1s, X2s, Zs), perm(Zs, Ys))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
ordered([]).
ordered(.(X, [])).
ordered(.(X, .(Y, Xs))) :- ','(less(X, s(Y)), ordered(.(Y, Xs))).
less(0, s(X)).
less(s(X), s(Y)) :- less(X, Y).

Queries:

ss(g,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

SS_IN(Xs, Ys) → U11(Xs, Ys, perm_in(Xs, Ys))
SS_IN(Xs, Ys) → PERM_IN(Xs, Ys)
PERM_IN(Xs, .(X, Ys)) → U31(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
PERM_IN(Xs, .(X, Ys)) → APP_IN(X1s, .(X, X2s), Xs)
APP_IN(.(X, Xs), Ys, .(X, Zs)) → U61(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U41(Xs, X, Ys, app_in(X1s, X2s, Zs))
U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → APP_IN(X1s, X2s, Zs)
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U51(Xs, X, Ys, perm_in(Zs, Ys))
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)
U11(Xs, Ys, perm_out(Xs, Ys)) → U21(Xs, Ys, ordered_in(Ys))
U11(Xs, Ys, perm_out(Xs, Ys)) → ORDERED_IN(Ys)
ORDERED_IN(.(X, .(Y, Xs))) → U71(X, Y, Xs, less_in(X, s(Y)))
ORDERED_IN(.(X, .(Y, Xs))) → LESS_IN(X, s(Y))
LESS_IN(s(X), s(Y)) → U91(X, Y, less_in(X, Y))
LESS_IN(s(X), s(Y)) → LESS_IN(X, Y)
U71(X, Y, Xs, less_out(X, s(Y))) → U81(X, Y, Xs, ordered_in(.(Y, Xs)))
U71(X, Y, Xs, less_out(X, s(Y))) → ORDERED_IN(.(Y, Xs))

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out
U41(x1, x2, x3, x4)  =  U41(x4)
ORDERED_IN(x1)  =  ORDERED_IN
PERM_IN(x1, x2)  =  PERM_IN
U91(x1, x2, x3)  =  U91(x3)
U61(x1, x2, x3, x4, x5)  =  U61(x5)
U71(x1, x2, x3, x4)  =  U71(x4)
U11(x1, x2, x3)  =  U11(x3)
APP_IN(x1, x2, x3)  =  APP_IN
SS_IN(x1, x2)  =  SS_IN(x1)
LESS_IN(x1, x2)  =  LESS_IN
U51(x1, x2, x3, x4)  =  U51(x4)
U31(x1, x2, x3, x4)  =  U31(x4)
U81(x1, x2, x3, x4)  =  U81(x4)
U21(x1, x2, x3)  =  U21(x3)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

SS_IN(Xs, Ys) → U11(Xs, Ys, perm_in(Xs, Ys))
SS_IN(Xs, Ys) → PERM_IN(Xs, Ys)
PERM_IN(Xs, .(X, Ys)) → U31(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
PERM_IN(Xs, .(X, Ys)) → APP_IN(X1s, .(X, X2s), Xs)
APP_IN(.(X, Xs), Ys, .(X, Zs)) → U61(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U41(Xs, X, Ys, app_in(X1s, X2s, Zs))
U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → APP_IN(X1s, X2s, Zs)
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U51(Xs, X, Ys, perm_in(Zs, Ys))
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)
U11(Xs, Ys, perm_out(Xs, Ys)) → U21(Xs, Ys, ordered_in(Ys))
U11(Xs, Ys, perm_out(Xs, Ys)) → ORDERED_IN(Ys)
ORDERED_IN(.(X, .(Y, Xs))) → U71(X, Y, Xs, less_in(X, s(Y)))
ORDERED_IN(.(X, .(Y, Xs))) → LESS_IN(X, s(Y))
LESS_IN(s(X), s(Y)) → U91(X, Y, less_in(X, Y))
LESS_IN(s(X), s(Y)) → LESS_IN(X, Y)
U71(X, Y, Xs, less_out(X, s(Y))) → U81(X, Y, Xs, ordered_in(.(Y, Xs)))
U71(X, Y, Xs, less_out(X, s(Y))) → ORDERED_IN(.(Y, Xs))

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out
U41(x1, x2, x3, x4)  =  U41(x4)
ORDERED_IN(x1)  =  ORDERED_IN
PERM_IN(x1, x2)  =  PERM_IN
U91(x1, x2, x3)  =  U91(x3)
U61(x1, x2, x3, x4, x5)  =  U61(x5)
U71(x1, x2, x3, x4)  =  U71(x4)
U11(x1, x2, x3)  =  U11(x3)
APP_IN(x1, x2, x3)  =  APP_IN
SS_IN(x1, x2)  =  SS_IN(x1)
LESS_IN(x1, x2)  =  LESS_IN
U51(x1, x2, x3, x4)  =  U51(x4)
U31(x1, x2, x3, x4)  =  U31(x4)
U81(x1, x2, x3, x4)  =  U81(x4)
U21(x1, x2, x3)  =  U21(x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 4 SCCs with 11 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

LESS_IN(s(X), s(Y)) → LESS_IN(X, Y)

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out
LESS_IN(x1, x2)  =  LESS_IN

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

LESS_IN(s(X), s(Y)) → LESS_IN(X, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESS_IN(x1, x2)  =  LESS_IN

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

LESS_IN → LESS_IN

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

LESS_IN → LESS_IN

The TRS R consists of the following rules:none


s = LESS_IN evaluates to t =LESS_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LESS_IN to LESS_IN.





↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U71(X, Y, Xs, less_out(X, s(Y))) → ORDERED_IN(.(Y, Xs))
ORDERED_IN(.(X, .(Y, Xs))) → U71(X, Y, Xs, less_in(X, s(Y)))

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out
ORDERED_IN(x1)  =  ORDERED_IN
U71(x1, x2, x3, x4)  =  U71(x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U71(X, Y, Xs, less_out(X, s(Y))) → ORDERED_IN(.(Y, Xs))
ORDERED_IN(.(X, .(Y, Xs))) → U71(X, Y, Xs, less_in(X, s(Y)))

The TRS R consists of the following rules:

less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
ORDERED_IN(x1)  =  ORDERED_IN
U71(x1, x2, x3, x4)  =  U71(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U71(less_out(X)) → ORDERED_IN
ORDERED_IN → U71(less_in)

The TRS R consists of the following rules:

less_in → U9(less_in)
less_in → less_out(0)
U9(less_out(X)) → less_out(s(X))

The set Q consists of the following terms:

less_in
U9(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule ORDERED_IN → U71(less_in) at position [0] we obtained the following new rules:

ORDERED_IN → U71(less_out(0))
ORDERED_IN → U71(U9(less_in))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ NonTerminationProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U71(less_out(X)) → ORDERED_IN
ORDERED_IN → U71(less_out(0))
ORDERED_IN → U71(U9(less_in))

The TRS R consists of the following rules:

less_in → U9(less_in)
less_in → less_out(0)
U9(less_out(X)) → less_out(s(X))

The set Q consists of the following terms:

less_in
U9(x0)

We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

U71(less_out(X)) → ORDERED_IN
ORDERED_IN → U71(less_out(0))
ORDERED_IN → U71(U9(less_in))

The TRS R consists of the following rules:

less_in → U9(less_in)
less_in → less_out(0)
U9(less_out(X)) → less_out(s(X))


s = ORDERED_IN evaluates to t =ORDERED_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

ORDERED_IN → U71(less_out(0))
with rule ORDERED_IN → U71(less_out(0)) at position [] and matcher [ ]

U71(less_out(0)) → ORDERED_IN
with rule U71(less_out(X)) → ORDERED_IN

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.





↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out
APP_IN(x1, x2, x3)  =  APP_IN

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APP_IN(x1, x2, x3)  =  APP_IN

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

APP_IN → APP_IN

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

APP_IN → APP_IN

The TRS R consists of the following rules:none


s = APP_IN evaluates to t =APP_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from APP_IN to APP_IN.





↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U41(Xs, X, Ys, app_in(X1s, X2s, Zs))
PERM_IN(Xs, .(X, Ys)) → U31(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out
U41(x1, x2, x3, x4)  =  U41(x4)
PERM_IN(x1, x2)  =  PERM_IN
U31(x1, x2, x3, x4)  =  U31(x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U41(Xs, X, Ys, app_in(X1s, X2s, Zs))
PERM_IN(Xs, .(X, Ys)) → U31(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)

The TRS R consists of the following rules:

app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U41(x1, x2, x3, x4)  =  U41(x4)
PERM_IN(x1, x2)  =  PERM_IN
U31(x1, x2, x3, x4)  =  U31(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U41(app_out) → PERM_IN
U31(app_out) → U41(app_in)
PERM_IN → U31(app_in)

The TRS R consists of the following rules:

app_in → U6(app_in)
app_in → app_out
U6(app_out) → app_out

The set Q consists of the following terms:

app_in
U6(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule U31(app_out) → U41(app_in) at position [0] we obtained the following new rules:

U31(app_out) → U41(U6(app_in))
U31(app_out) → U41(app_out)



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U41(app_out) → PERM_IN
U31(app_out) → U41(U6(app_in))
U31(app_out) → U41(app_out)
PERM_IN → U31(app_in)

The TRS R consists of the following rules:

app_in → U6(app_in)
app_in → app_out
U6(app_out) → app_out

The set Q consists of the following terms:

app_in
U6(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule PERM_IN → U31(app_in) at position [0] we obtained the following new rules:

PERM_IN → U31(app_out)
PERM_IN → U31(U6(app_in))



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ NonTerminationProof
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U41(app_out) → PERM_IN
PERM_IN → U31(app_out)
PERM_IN → U31(U6(app_in))
U31(app_out) → U41(U6(app_in))
U31(app_out) → U41(app_out)

The TRS R consists of the following rules:

app_in → U6(app_in)
app_in → app_out
U6(app_out) → app_out

The set Q consists of the following terms:

app_in
U6(x0)

We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

U41(app_out) → PERM_IN
PERM_IN → U31(app_out)
PERM_IN → U31(U6(app_in))
U31(app_out) → U41(U6(app_in))
U31(app_out) → U41(app_out)

The TRS R consists of the following rules:

app_in → U6(app_in)
app_in → app_out
U6(app_out) → app_out


s = PERM_IN evaluates to t =PERM_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

PERM_IN → U31(app_out)
with rule PERM_IN → U31(app_out) at position [] and matcher [ ]

U31(app_out) → U41(app_out)
with rule U31(app_out) → U41(app_out) at position [] and matcher [ ]

U41(app_out) → PERM_IN
with rule U41(app_out) → PERM_IN

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.




We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x1, x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x1, x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x1, x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x1, x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out(x1)


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

SS_IN(Xs, Ys) → U11(Xs, Ys, perm_in(Xs, Ys))
SS_IN(Xs, Ys) → PERM_IN(Xs, Ys)
PERM_IN(Xs, .(X, Ys)) → U31(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
PERM_IN(Xs, .(X, Ys)) → APP_IN(X1s, .(X, X2s), Xs)
APP_IN(.(X, Xs), Ys, .(X, Zs)) → U61(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U41(Xs, X, Ys, app_in(X1s, X2s, Zs))
U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → APP_IN(X1s, X2s, Zs)
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U51(Xs, X, Ys, perm_in(Zs, Ys))
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)
U11(Xs, Ys, perm_out(Xs, Ys)) → U21(Xs, Ys, ordered_in(Ys))
U11(Xs, Ys, perm_out(Xs, Ys)) → ORDERED_IN(Ys)
ORDERED_IN(.(X, .(Y, Xs))) → U71(X, Y, Xs, less_in(X, s(Y)))
ORDERED_IN(.(X, .(Y, Xs))) → LESS_IN(X, s(Y))
LESS_IN(s(X), s(Y)) → U91(X, Y, less_in(X, Y))
LESS_IN(s(X), s(Y)) → LESS_IN(X, Y)
U71(X, Y, Xs, less_out(X, s(Y))) → U81(X, Y, Xs, ordered_in(.(Y, Xs)))
U71(X, Y, Xs, less_out(X, s(Y))) → ORDERED_IN(.(Y, Xs))

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x1, x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x1, x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out(x1)
U41(x1, x2, x3, x4)  =  U41(x4)
ORDERED_IN(x1)  =  ORDERED_IN
PERM_IN(x1, x2)  =  PERM_IN
U91(x1, x2, x3)  =  U91(x3)
U61(x1, x2, x3, x4, x5)  =  U61(x5)
U71(x1, x2, x3, x4)  =  U71(x4)
U11(x1, x2, x3)  =  U11(x1, x3)
APP_IN(x1, x2, x3)  =  APP_IN
SS_IN(x1, x2)  =  SS_IN(x1)
LESS_IN(x1, x2)  =  LESS_IN
U51(x1, x2, x3, x4)  =  U51(x4)
U31(x1, x2, x3, x4)  =  U31(x4)
U81(x1, x2, x3, x4)  =  U81(x4)
U21(x1, x2, x3)  =  U21(x1, x3)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

SS_IN(Xs, Ys) → U11(Xs, Ys, perm_in(Xs, Ys))
SS_IN(Xs, Ys) → PERM_IN(Xs, Ys)
PERM_IN(Xs, .(X, Ys)) → U31(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
PERM_IN(Xs, .(X, Ys)) → APP_IN(X1s, .(X, X2s), Xs)
APP_IN(.(X, Xs), Ys, .(X, Zs)) → U61(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)
U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U41(Xs, X, Ys, app_in(X1s, X2s, Zs))
U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → APP_IN(X1s, X2s, Zs)
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U51(Xs, X, Ys, perm_in(Zs, Ys))
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)
U11(Xs, Ys, perm_out(Xs, Ys)) → U21(Xs, Ys, ordered_in(Ys))
U11(Xs, Ys, perm_out(Xs, Ys)) → ORDERED_IN(Ys)
ORDERED_IN(.(X, .(Y, Xs))) → U71(X, Y, Xs, less_in(X, s(Y)))
ORDERED_IN(.(X, .(Y, Xs))) → LESS_IN(X, s(Y))
LESS_IN(s(X), s(Y)) → U91(X, Y, less_in(X, Y))
LESS_IN(s(X), s(Y)) → LESS_IN(X, Y)
U71(X, Y, Xs, less_out(X, s(Y))) → U81(X, Y, Xs, ordered_in(.(Y, Xs)))
U71(X, Y, Xs, less_out(X, s(Y))) → ORDERED_IN(.(Y, Xs))

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x1, x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x1, x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out(x1)
U41(x1, x2, x3, x4)  =  U41(x4)
ORDERED_IN(x1)  =  ORDERED_IN
PERM_IN(x1, x2)  =  PERM_IN
U91(x1, x2, x3)  =  U91(x3)
U61(x1, x2, x3, x4, x5)  =  U61(x5)
U71(x1, x2, x3, x4)  =  U71(x4)
U11(x1, x2, x3)  =  U11(x1, x3)
APP_IN(x1, x2, x3)  =  APP_IN
SS_IN(x1, x2)  =  SS_IN(x1)
LESS_IN(x1, x2)  =  LESS_IN
U51(x1, x2, x3, x4)  =  U51(x4)
U31(x1, x2, x3, x4)  =  U31(x4)
U81(x1, x2, x3, x4)  =  U81(x4)
U21(x1, x2, x3)  =  U21(x1, x3)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 4 SCCs with 11 less nodes.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LESS_IN(s(X), s(Y)) → LESS_IN(X, Y)

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x1, x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x1, x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out(x1)
LESS_IN(x1, x2)  =  LESS_IN

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

LESS_IN(s(X), s(Y)) → LESS_IN(X, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESS_IN(x1, x2)  =  LESS_IN

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

LESS_IN → LESS_IN

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

LESS_IN → LESS_IN

The TRS R consists of the following rules:none


s = LESS_IN evaluates to t =LESS_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from LESS_IN to LESS_IN.





↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U71(X, Y, Xs, less_out(X, s(Y))) → ORDERED_IN(.(Y, Xs))
ORDERED_IN(.(X, .(Y, Xs))) → U71(X, Y, Xs, less_in(X, s(Y)))

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x1, x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x1, x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out(x1)
ORDERED_IN(x1)  =  ORDERED_IN
U71(x1, x2, x3, x4)  =  U71(x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

U71(X, Y, Xs, less_out(X, s(Y))) → ORDERED_IN(.(Y, Xs))
ORDERED_IN(.(X, .(Y, Xs))) → U71(X, Y, Xs, less_in(X, s(Y)))

The TRS R consists of the following rules:

less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
ORDERED_IN(x1)  =  ORDERED_IN
U71(x1, x2, x3, x4)  =  U71(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U71(less_out(X)) → ORDERED_IN
ORDERED_IN → U71(less_in)

The TRS R consists of the following rules:

less_in → U9(less_in)
less_in → less_out(0)
U9(less_out(X)) → less_out(s(X))

The set Q consists of the following terms:

less_in
U9(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule ORDERED_IN → U71(less_in) at position [0] we obtained the following new rules:

ORDERED_IN → U71(less_out(0))
ORDERED_IN → U71(U9(less_in))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ NonTerminationProof
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

U71(less_out(X)) → ORDERED_IN
ORDERED_IN → U71(less_out(0))
ORDERED_IN → U71(U9(less_in))

The TRS R consists of the following rules:

less_in → U9(less_in)
less_in → less_out(0)
U9(less_out(X)) → less_out(s(X))

The set Q consists of the following terms:

less_in
U9(x0)

We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

U71(less_out(X)) → ORDERED_IN
ORDERED_IN → U71(less_out(0))
ORDERED_IN → U71(U9(less_in))

The TRS R consists of the following rules:

less_in → U9(less_in)
less_in → less_out(0)
U9(less_out(X)) → less_out(s(X))


s = ORDERED_IN evaluates to t =ORDERED_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

ORDERED_IN → U71(less_out(0))
with rule ORDERED_IN → U71(less_out(0)) at position [] and matcher [ ]

U71(less_out(0)) → ORDERED_IN
with rule U71(less_out(X)) → ORDERED_IN

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.





↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x1, x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x1, x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out(x1)
APP_IN(x1, x2, x3)  =  APP_IN

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

APP_IN(.(X, Xs), Ys, .(X, Zs)) → APP_IN(Xs, Ys, Zs)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APP_IN(x1, x2, x3)  =  APP_IN

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ NonTerminationProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

APP_IN → APP_IN

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

APP_IN → APP_IN

The TRS R consists of the following rules:none


s = APP_IN evaluates to t =APP_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from APP_IN to APP_IN.





↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U41(Xs, X, Ys, app_in(X1s, X2s, Zs))
PERM_IN(Xs, .(X, Ys)) → U31(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)

The TRS R consists of the following rules:

ss_in(Xs, Ys) → U1(Xs, Ys, perm_in(Xs, Ys))
perm_in(Xs, .(X, Ys)) → U3(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))
U3(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U4(Xs, X, Ys, app_in(X1s, X2s, Zs))
U4(Xs, X, Ys, app_out(X1s, X2s, Zs)) → U5(Xs, X, Ys, perm_in(Zs, Ys))
perm_in([], []) → perm_out([], [])
U5(Xs, X, Ys, perm_out(Zs, Ys)) → perm_out(Xs, .(X, Ys))
U1(Xs, Ys, perm_out(Xs, Ys)) → U2(Xs, Ys, ordered_in(Ys))
ordered_in(.(X, .(Y, Xs))) → U7(X, Y, Xs, less_in(X, s(Y)))
less_in(s(X), s(Y)) → U9(X, Y, less_in(X, Y))
less_in(0, s(X)) → less_out(0, s(X))
U9(X, Y, less_out(X, Y)) → less_out(s(X), s(Y))
U7(X, Y, Xs, less_out(X, s(Y))) → U8(X, Y, Xs, ordered_in(.(Y, Xs)))
ordered_in(.(X, [])) → ordered_out(.(X, []))
ordered_in([]) → ordered_out([])
U8(X, Y, Xs, ordered_out(.(Y, Xs))) → ordered_out(.(X, .(Y, Xs)))
U2(Xs, Ys, ordered_out(Ys)) → ss_out(Xs, Ys)

The argument filtering Pi contains the following mapping:
ss_in(x1, x2)  =  ss_in(x1)
U1(x1, x2, x3)  =  U1(x1, x3)
perm_in(x1, x2)  =  perm_in
.(x1, x2)  =  .(x1, x2)
U3(x1, x2, x3, x4)  =  U3(x4)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U4(x1, x2, x3, x4)  =  U4(x4)
U5(x1, x2, x3, x4)  =  U5(x4)
perm_out(x1, x2)  =  perm_out
U2(x1, x2, x3)  =  U2(x1, x3)
ordered_in(x1)  =  ordered_in
U7(x1, x2, x3, x4)  =  U7(x4)
less_in(x1, x2)  =  less_in
s(x1)  =  s(x1)
U9(x1, x2, x3)  =  U9(x3)
0  =  0
less_out(x1, x2)  =  less_out(x1)
U8(x1, x2, x3, x4)  =  U8(x4)
ordered_out(x1)  =  ordered_out
ss_out(x1, x2)  =  ss_out(x1)
U41(x1, x2, x3, x4)  =  U41(x4)
PERM_IN(x1, x2)  =  PERM_IN
U31(x1, x2, x3, x4)  =  U31(x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

U31(Xs, X, Ys, app_out(X1s, .(X, X2s), Xs)) → U41(Xs, X, Ys, app_in(X1s, X2s, Zs))
PERM_IN(Xs, .(X, Ys)) → U31(Xs, X, Ys, app_in(X1s, .(X, X2s), Xs))
U41(Xs, X, Ys, app_out(X1s, X2s, Zs)) → PERM_IN(Zs, Ys)

The TRS R consists of the following rules:

app_in(.(X, Xs), Ys, .(X, Zs)) → U6(X, Xs, Ys, Zs, app_in(Xs, Ys, Zs))
app_in([], X, X) → app_out([], X, X)
U6(X, Xs, Ys, Zs, app_out(Xs, Ys, Zs)) → app_out(.(X, Xs), Ys, .(X, Zs))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
app_in(x1, x2, x3)  =  app_in
U6(x1, x2, x3, x4, x5)  =  U6(x5)
[]  =  []
app_out(x1, x2, x3)  =  app_out
U41(x1, x2, x3, x4)  =  U41(x4)
PERM_IN(x1, x2)  =  PERM_IN
U31(x1, x2, x3, x4)  =  U31(x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U41(app_out) → PERM_IN
U31(app_out) → U41(app_in)
PERM_IN → U31(app_in)

The TRS R consists of the following rules:

app_in → U6(app_in)
app_in → app_out
U6(app_out) → app_out

The set Q consists of the following terms:

app_in
U6(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule U31(app_out) → U41(app_in) at position [0] we obtained the following new rules:

U31(app_out) → U41(U6(app_in))
U31(app_out) → U41(app_out)



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

U41(app_out) → PERM_IN
U31(app_out) → U41(U6(app_in))
U31(app_out) → U41(app_out)
PERM_IN → U31(app_in)

The TRS R consists of the following rules:

app_in → U6(app_in)
app_in → app_out
U6(app_out) → app_out

The set Q consists of the following terms:

app_in
U6(x0)

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule PERM_IN → U31(app_in) at position [0] we obtained the following new rules:

PERM_IN → U31(app_out)
PERM_IN → U31(U6(app_in))



↳ Prolog
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ Narrowing
                          ↳ QDP
                            ↳ Narrowing
                              ↳ QDP
                                ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

U41(app_out) → PERM_IN
PERM_IN → U31(app_out)
PERM_IN → U31(U6(app_in))
U31(app_out) → U41(U6(app_in))
U31(app_out) → U41(app_out)

The TRS R consists of the following rules:

app_in → U6(app_in)
app_in → app_out
U6(app_out) → app_out

The set Q consists of the following terms:

app_in
U6(x0)

We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

U41(app_out) → PERM_IN
PERM_IN → U31(app_out)
PERM_IN → U31(U6(app_in))
U31(app_out) → U41(U6(app_in))
U31(app_out) → U41(app_out)

The TRS R consists of the following rules:

app_in → U6(app_in)
app_in → app_out
U6(app_out) → app_out


s = PERM_IN evaluates to t =PERM_IN

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

PERM_IN → U31(app_out)
with rule PERM_IN → U31(app_out) at position [] and matcher [ ]

U31(app_out) → U41(app_out)
with rule U31(app_out) → U41(app_out) at position [] and matcher [ ]

U41(app_out) → PERM_IN
with rule U41(app_out) → PERM_IN

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.